#include "formule.hpp"

////////////////////////////////////////////////////////////////////////////////
//            A PARTIR D'ICI LES FONCTIONS SONT A IMPLEMENTER                 //
////////////////////////////////////////////////////////////////////////////////
ostream& operator<<(ostream& out, const cls_t& cl)
{
	for(cls_t::const_iterator it= cl.begin();it!=cl.end();it++)
	{
		out<<" " <<*it <<" ";
	}
	cout<<endl;
	//  out << "{" << 42 << '}' << endl;
	return out;
}

ostream& operator<<(ostream& out, const cnf_t& c)
{
	for(cnf_t::const_iterator it= c.begin();it!=c.end();it++)
	{
		operator<<(out, *it);
	}
	return out;
}


bool est_dans(const cls_t& c, const cnf_t& f)
{
	if(!f.empty()) // Si f est vide, il n'y a pas d'autres tests à faire
	{
		for(int i=0;i<(int)f.size();i++)
		{
			if (f[i]==c)
				return true;

		}
		//cls_t::const_iterator location=find(f.begin(),f.end(),c);
		//if (location != f.end())
			//	return true;
		return false;
	}
	return false;
}

lit_t var2lit(var_t v, bool p)
{
	if(!p)	
		return 2*v+1;
	return 2*v;
}

lit_t neg(lit_t l)
{
	if (positif(l))
		return l+1;
	return l-1;
}


var_t lit2var(lit_t l) 
{
	if (positif(l))
		return(l/2);
	return((l-1)/2);
}

bool positif(lit_t l) 
{
	if((l%2)==1)
		return false;
	return true;
}


